use "../Common/bkj.ml";

(* structure which implements a context graph data structure, including it's supported operations *) 
signature CONTEXT_GRAPH =
  sig
	(* this "global" variable stores the number of hash table buckets in graphs created through the newGraph() function.  
	    in order to improve performance - it should be initialized to at least 2^X, where X is the number of variables in the analysed program. *)
    val numBuckets : int ref

	(* a flag to turn on/off debug info printing *)
	val debug : bool ref

	(* a hash table structure with string keys *)	
	structure HshTbl : MONO_HASH_TABLE   

	(* a variable set representation as a bit field *)
	type Context 
	
	(* the data which is hanging on the context graph edges *)
	type edgeTag = sop_bar.DFR ref

	(*the graph type - it is actually a hash table with string keys *)
	type graph = edgeTag HshTbl.hash_table

	(* a tagged (E) or untagged (UE) edge datatype *)
    datatype edge = E of Context * Context * edgeTag | UE of Context * Context

	(* returns the specified edge's source context *)
    val edgeSrc : edge -> Context
	(* returns the specified edge's target context *)
    val edgeTgt : edge -> Context
	(* creates a unique string key for the edge *)
    val edgeToHash : edge -> string
	(* creates an untagged (UE) edge from a unique string key *)
    val hashToEdge : string -> edge
	(* 1. If edge exists in g - updates exiting edge's DFR to be: LUB(existing_DFR,  new_DFR) .
	   2. Otherwise, adds the new edge to g.*)	
    val addEdge : graph * edge -> unit
	(* inserts a list of edges to the graph g. 
	    If a specified edge is already in g, the new edge's DFR will be joined with the existing edge's DFR *)
    val addEdges : graph * edge list -> unit

	(* constructor for new graphs - creates a new graph given the specified edge list *)
    val newGraph : edge list -> graph
 
	(* returns the edge tag of the specified edge *)
	val getEdgeTag : graph * edge -> edgeTag option
	(* returns a list of all edges in graph - not including edge tags (UE edge constructor is used to create each edge) *)
    val untaggedEdges : graph -> edge list
	(* returns all edges in graph including edge tags (E edge constructor is usedto create each edge) *)
    val edges : graph -> edge list
	
	(* creates an empty context which can hold up to the specified number of variables *)
    val makeEmptyContext : int -> Context
 	(* creates a context which can hold up to the specified number of variables and is filled with the specified list of variable indices *)
    val makeContext : int * int list -> Context
	
	(* returns a copy of the srcContext, assuming that numVars is the number of variables in srcContext *)
	val copyContext : int * Context -> Context
	
	(* adds variable with index x to context c *)
	val addVarToContext : int * Context -> unit 

	(* removes variable with index x from context c *)	
	val removeVarFromContext : int * Context -> unit

	(* if 'add' is true - adds x to context c, otherwise removes x from context c *)
	val setVarInContext : int * Context * bool -> unit
	
	val contextToVarList : Context -> int list 
    val inContext : int * Context -> BitArray.elem
	(* outputs the context's variables to a nicely formatted string. *)	
	val prtContext : Context -> string
	
 	(* a partial order on edges, based on lexicographic ordering of the source and target contexts. *)	
	val edgeSmaller : edge * edge -> bool
	(* Inserts an edge into a sorted list of edges *)		
    val insertEdge : edge * edge list -> edge list
	(* Sorts a list of edges *)			
    val sortEdges : edge list -> edge list
 	(* outputs the edge context variables and DFR to a nicely formatted string. *)	
    val prtEdge : edge -> string
	(* for all edge in the list - outputs the edge context variables and DFR to a nicely formatted string. *)	
    val prtEdgeList : edge list -> string
	(* for all edge in the graph - outputs the edge context variables and DFR to a nicely formatted string. *)	
    val prtEdges : graph -> string
	(* for all edge in the graph - outputs the edge context variables and DFR to a nicely formatted string. *)	
    val printEdges : graph -> unit
	(* returns a list of contexts which are the the post contexts of all edges in graph *)
	val postContexts : graph -> Context list;
	(* returns a copy of the graph *)
	val clone : graph -> graph
	
	(* returns true iff context c1 is equal to context c2. *)
	val  eqContexts : Context * Context -> bool
    (* returns true if graphs are equal - e.g. have the same edges and same edge tags on all edges *)
    val equal : graph * graph -> bool

	(* computes all possible contexts (except the full context) over a set of variables, 
	   where highestVar is the highest variable index *) 
	val allContexts : int -> Context list 

	(* joins the graph g with a graph which has the same edges and on each edge it holds the identity DFR *)
	val complementToIdentityOnExistingEdges : int * graph ref -> unit

	(* compute the composition of two graphs *)
    val compose : graph * graph -> graph
	(* computes the join (LUB) of two graphs *)	
    val join : graph * graph -> graph
  end (* signature CG *)
  
